\begin{tipo}{Gateway}
	\observador{numero}{g: Gateway}{Numero}
	\observador{trivias}{g: Gateway}{[Trivia]}
	\observador{comandos}{g: Gateway}{[Keyword]}
		
	\medskip
	\invariante[sinTriviasRepetidas]{sinRepetidos(trivias(g))}
	\invariante[sinComandosRepetidos]{sinRepetidos(comandos(g))}
	\invariante[noSeSuperponenTrivias]{(\forall t_1, t_2 \selec trivias(g)) \longitud{interseccion(keywords(t_1), keywords(t_2))} == 0}
	\invariante[noSeSolapanComandosConTrivias]{ (\forall x \selec trivias(g))
	\longitud{interseccion(comandos(g),keywords(x))} == 0}
	\invariante[comandosSinEspacios]{(\forall c \selec comandos(g)) sinEspacios(c)}
	
\end{tipo}